ITT n
$ \mathrm{ITT}_n
Per Martin-Löfが構成した型理論の一つ
自然数全体の型$ Nや、Π-規則などから推論規則を繰り返し用いて作られる型のみを扱う
predicativeな型理論